Inference at * 
Iof proof for Lemma append overlapping sublists:


  T:Type, L1, L2, L:(T List), x:T.
  no_repeats(T;L)  L1 @ [x]  L  [x / L2]  L  L1 @ [x / L2]  L 

latex

 by (((((((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)) 

 bCollapseTHEN (All (Unfolds ``sublist no_repeats``)))) 
CollapseTHEN (All Reduce))) 

CoCollapseTHEN (ExRepD)) 

latex

C1: 

C1: 1. T : Type
C1: 2. L1 : T List
C1: 3. L2 : T List
C1: 4. L : T List
C1: 5. x : T
C1: 6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
C1: 7. f1 : {0..||L1 @ [x]||}{0..||L||}
C1: 8. increasing(f1;||L1 @ [x]||)
C1: 9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
C1: 10. f : {0..(||L2||+1)}{0..||L||}
C1: 11. increasing(f;||L2||+1)
C1: 12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
C1:   f:{0..||L1 @ [x / L2]||}{0..||L||}
C1:   (increasing(f;||L1 @ [x / L2]||)
C1:   & (j:{0..||L1 @ [x / L2]||}. (L1 @ [x / L2])[j] = L[(f(j))]))
C.

Definitions	t  T, L1  L2, P  Q, x:A. B(x), Y, P & Q, ||as||, x:A. B(x), no_repeats(T;l),
Lemmas	no repeats wf, append wf, sublist wf